es:ES, ff:FIFO, j, i:ff.C, e:{e:E| ff.S(j,i,e)} . (e < ff.Receiver(j,i,e)) 

latex

Definitions	x:A. B(x), t  T, , t  ...$L, e c e', P  Q, P  Q
Lemmas	es-E wf, fifoS wf, fifoC wf, FIFO wf, event system wf, fifoReceiver-properties, fifoSender-causes, fifoReceiver wf, es-causl transitivity1, fifoR wf, es-causl wf